Nuprl Definition : w-V 11,40

V(i;k) == kindcase(ka.((w.2).1)(i,a); l,tg.((w.2.2).1)(l,tg) ) 
latex



clarification:

w-V(wik) == kindcase(ka.((w.2).1)(i,a); l,tg.((w.2.2).1)(l,tg) ) 
latex


Definitionskindcase(ka.f(a); l,t.g(l;t) ), f(a), t.1, t.2
FDL editor aliasesw-V

origin